/*
 * $Id: FractalStaticChecker.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 * 
 */
package org.objectweb.fractal.bpc.checker;


import org.objectweb.fractal.bpc.checker.DFSR.Options;
import org.objectweb.fractal.bpc.checker.backend.*;
import org.objectweb.fractal.bpc.checker.node.*;
import org.objectweb.fractal.bpc.checker.parser.*;

/**
 * This is implementation of Static Protocol Checker for Fractal. 
 * Frame with Architecture protocols can be checked.
 */
public class FractalStaticChecker {

    /** Creates a new instance of Fractal */
    public FractalStaticChecker() {
    }


    /**
     * This method perform the compliance check using the consent operator.
     * 
     * @param frameprot the frame protocol.
     * @param synchrooperations operation of the bounded interfaces on the binding between the frame and architecture and among the protocols in the same order as the protocols appears in the following parameter. 
     * @param subcomponents the protocols of subcomponents 
     * @param unboundmethods methods of interfaces that are not bound.
     * 
     * @return the checking result.
     */
    public CheckingResult check(String frameprot, String[] synchrooperations, String[] subcomponents, String unboundmethods) {
        
        //return new CheckingResult(CheckingResult.ERR_OK, null);

		
        Debug.setLevel(0);


        //basic checks;
        if ((synchrooperations == null) ||
            (subcomponents == null) ||
            (synchrooperations.length != subcomponents.length) ||
            (frameprot == null) ||
            (unboundmethods == null))
            	return new CheckingResult(CheckingResult.ERR_SYNTAXERROR, "Static checker: Input arguments not well formed (possible null pointer among them"); 
        
        ActionRepository repository = new ActionRepository();
        
        // debug
        Debug.println(1, "Frame protocol:");
        Debug.println(1, frameprot);
        
        for (int i = 0; i < synchrooperations.length; ++i) {
        	  Debug.println(1, "Synchro:");
        	  Debug.println(1, synchrooperations[i]);
        	  Debug.println(1, "Protocol:");
        	  Debug.println(1, subcomponents[i]);
        }
         

        
        // creating the field of protocols and synchro operations for parsing
        String[] inputdata = new String[2 * subcomponents.length + 2];

        inputdata[0] = frameprot;
        for (int i = 0; i < synchrooperations.length; ++i) {
            inputdata[(2*i) + 1] = synchrooperations[i];
            inputdata[(2*i) + 2] = subcomponents[i];
        }
        
        inputdata[inputdata.length - 1] = unboundmethods;
        
        // parsing the protocols
        Object[] parsed;
        
        try {
            parsed = StandaloneMain.buildTrees(inputdata, repository);
        }
        catch (SyntaxErrorException e) {
            return new CheckingResult(CheckingResult.ERR_SYNTAXERROR, e.getMessage());
        }
        
        TreeNode[] nodes = (TreeNode[]) parsed[0];
        String[] provs = (String[]) parsed[1];
        String unbound = (String) parsed[2];
        


        // setting up the options of checking
        Options.action = Options.ACTIONTESTCOMPLIANCE;
        Options.badactivity = true;
        Options.noactivity = true;
        Options.infiniteactivity = Options.IANO;
        Options.statememory = 100000;

        // checking compliance
        return new ConsentBackend(repository).perform(nodes, provs, unbound.equals("") ? new String[0] : unbound.split(","));
		
    }
}
